Inference at * 1 
Iof proof for Lemma lt int eq false elim:



1. i : 
2. j : 
3. i <z j = ff
  (i < j) 

latex

 by InteriorProof ((RW bool_to_propC 3) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
CollapseTHEN ((Aut),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	P  Q, P & Q, T, P  Q, False, P  Q, A, True, , t  T, A  B, x:A. B(x)
Lemmas	assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, iff transitivity, bnot wf, le wf, le int wf, assert wf, bool wf